
\documentclass[runningheads]{llncs}
\usepackage{stmaryrd}
\usepackage{amsfonts}

\usepackage{amssymb}
\setcounter{tocdepth}{3}
\usepackage{graphicx}
\usepackage{algorithmic, algorithm}

\usepackage{url}
\newcommand{\keywords}[1]{\par\addvspace\baselineskip
\noindent\keywordname\enspace\ignorespaces#1}

\begin{document}

\mainmatter  % start of an individual contribution

% first the title is needed
\title{Use Coq and Model Checking to Build Reliable PLC Application}

% a short form should be given in case it is too long for the running head
\titlerunning{Use Coq and Model Checking to Build Reliable PLC Applications}

% the name(s) of the author(s) follow(s) next
%
% NB: Chinese authors should write their first names(s) in front of
% their surnames. This ensures that the names appear correctly in
% the running heads and the author index.
%
\author{}
%
\authorrunning{}
% (feature abused for this document to repeat the title also on left hand pages)

% the affiliations are given next; don't give your e-mail address
% unless you accept that it will be published
\institute{}

\toctitle{} \tocauthor{} \maketitle


\begin{abstract}

This paper presents a method that can be used to build reliable PLC
applications. The method combines the advantages of the theorem
prover Coq and model checking technology. It uses Coq to model and
verify properties. It uses translation validation with timers to
check whether the PLC codes implement the abstract model correctly.


\keywords{PLC, Coq, Model Checking, Reliable Application}
\end{abstract}

\section{Introduction}

PLC (programmable logic controller) is a equipment used for
real-time embedded system\cite{s7-200-manual}.

PLC applications with timers are difficult to verify.

Timed automata is a powerful tool to do modeling and verification.

Since Coq is based on higher order logic, it is powerful enough to
model PLC application in detail.

\section{The Method}

\subsection{The Abstract Model and Its Verification}

\subsection{The Concrete Model and Its Validation}

The method is divided into two parts. First we build the abstract
model based on the specification of the problem.

\section{Case Study}

\subsection{Quiz Machine}

\subsection{Abstract Model and Its Verification}

\subsection{The Concrete Model and Its Validation}


\section{Conclusions}

\bibliographystyle{splncs}
\bibliography{ref}


\end{document}
